Nuprl Lemma : es-fix-cases
11,40
postcript
pdf
es
,
f
,
e
:Top.
f
**(
e
) ~ if
e
=
f
(
e
) then
e
else
f
**(
f
(
e
)) fi
latex
Definitions
s
~
t
,
Top
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
t
T
,
s
=
t
,
f
**(
e
)
,
es-eq(
es
)
Lemmas
top
wf
origin
es, f, e:Top. f**(e) ~ if e = f(e) then e else f**(f(e)) fi es, f, e:Top. f**(e) ~ if e = f(e) then e else f**(f(e)) fi x:A. B(x)
B(x)
T